'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))
, t^#(s(x1)) -> c_5(t^#(t(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
The usable rules are:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))}
The estimated dependency graph contains the following edges:
{s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
==> {b^#(u(x1)) -> c_4(b^#(s(x1)))}
{s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
==> {b^#(u(x1)) -> c_4(b^#(s(x1)))}
{t^#(b(x1)) -> c_2(b^#(s(x1)))}
==> {b^#(u(x1)) -> c_4(b^#(s(x1)))}
{t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
==> {t^#(u(x1)) -> c_6(t^#(x1))}
{t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
==> {t^#(s(x1)) -> c_5(t^#(t(x1)))}
{t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
==> {t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
{t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
==> {t^#(b(x1)) -> c_2(b^#(s(x1)))}
{b^#(u(x1)) -> c_4(b^#(s(x1)))}
==> {b^#(u(x1)) -> c_4(b^#(s(x1)))}
{t^#(s(x1)) -> c_5(t^#(t(x1)))}
==> {t^#(u(x1)) -> c_6(t^#(x1))}
{t^#(s(x1)) -> c_5(t^#(t(x1)))}
==> {t^#(s(x1)) -> c_5(t^#(t(x1)))}
{t^#(s(x1)) -> c_5(t^#(t(x1)))}
==> {t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
{t^#(s(x1)) -> c_5(t^#(t(x1)))}
==> {t^#(b(x1)) -> c_2(b^#(s(x1)))}
{t^#(u(x1)) -> c_6(t^#(x1))}
==> {t^#(u(x1)) -> c_6(t^#(x1))}
{t^#(u(x1)) -> c_6(t^#(x1))}
==> {t^#(s(x1)) -> c_5(t^#(t(x1)))}
{t^#(u(x1)) -> c_6(t^#(x1))}
==> {t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
{t^#(u(x1)) -> c_6(t^#(x1))}
==> {t^#(b(x1)) -> c_2(b^#(s(x1)))}
{s^#(u(x1)) -> c_7(s^#(s(x1)))}
==> {s^#(u(x1)) -> c_7(s^#(s(x1)))}
{s^#(u(x1)) -> c_7(s^#(s(x1)))}
==> {s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
{s^#(u(x1)) -> c_7(s^#(s(x1)))}
==> {s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
We consider the following path(s):
1) { t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))}
The usable rules for this path are the following:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [1]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{t(b(s(x1))) -> u(t(b(x1)))}
and weakly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{t(b(s(x1))) -> u(t(b(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [0]
c_2(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))}
and weakly orienting the rules
{ t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [7]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
and weakly orienting the rules
{ t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))
, t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [1]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [3]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [8]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))}
Weak Rules:
{ t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))
, t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))}
Weak Rules:
{ t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))
, t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ u_0(4) -> 4
, b^#_0(4) -> 7
, t^#_0(4) -> 9
, c_6_0(9) -> 9}
2) { t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))
, t^#(b(x1)) -> c_2(b^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
The usable rules for this path are the following:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, t^#(b(x1)) -> c_2(b^#(s(x1)))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [1]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{t(b(s(x1))) -> u(t(b(x1)))}
and weakly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{t(b(s(x1))) -> u(t(b(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [1]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{t^#(b(x1)) -> c_2(b^#(s(x1)))}
and weakly orienting the rules
{ t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{t^#(b(x1)) -> c_2(b^#(s(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [9]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [1] x1 + [15]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Weak Rules:
{ t^#(b(x1)) -> c_2(b^#(s(x1)))
, t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Weak Rules:
{ t^#(b(x1)) -> c_2(b^#(s(x1)))
, t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ s_1(2) -> 4
, s_1(4) -> 4
, u_0(2) -> 2
, b^#_0(2) -> 1
, b^#_1(4) -> 3
, t^#_0(2) -> 1
, c_4_1(3) -> 1
, c_6_0(1) -> 1}
3) { s^#(u(x1)) -> c_7(s^#(s(x1)))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
The usable rules for this path are the following:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [1]
s^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [1]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
and weakly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [2]
s^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
and weakly orienting the rules
{ s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [8]
s^#(x1) = [1] x1 + [2]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(u(x1)) -> u(t(x1))}
Weak Rules:
{ s^#(b(s(x1))) -> c_1(b^#(t(x1)))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(u(x1)) -> u(t(x1))}
Weak Rules:
{ s^#(b(s(x1))) -> c_1(b^#(t(x1)))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ s_0(4) -> 9
, s_0(9) -> 9
, u_0(4) -> 4
, s^#_0(4) -> 5
, s^#_0(9) -> 8
, b^#_0(4) -> 7
, b^#_0(9) -> 10
, c_4_0(10) -> 7
, c_7_0(8) -> 5}
4) { t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
The usable rules for this path are the following:
{ t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, t^#(u(x1)) -> c_6(t^#(x1))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{t(b(x1)) -> b(s(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{t(b(x1)) -> b(s(x1))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [0]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(u(x1)) -> b(s(x1))
, s(u(x1)) -> s(s(x1))
, t^#(u(x1)) -> c_6(t^#(x1))}
and weakly orienting the rules
{t(b(x1)) -> b(s(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(u(x1)) -> b(s(x1))
, s(u(x1)) -> s(s(x1))
, t^#(u(x1)) -> c_6(t^#(x1))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [8]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [15]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
and weakly orienting the rules
{ b(u(x1)) -> b(s(x1))
, s(u(x1)) -> s(s(x1))
, t^#(u(x1)) -> c_6(t^#(x1))
, t(b(x1)) -> b(s(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [6]
b(x1) = [1] x1 + [12]
t(x1) = [1] x1 + [6]
u(x1) = [1] x1 + [8]
s^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [8]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(b(x1)) -> b(s(s(s(x1))))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
Weak Rules:
{ s(b(s(x1))) -> b(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, b(u(x1)) -> b(s(x1))
, s(u(x1)) -> s(s(x1))
, t^#(u(x1)) -> c_6(t^#(x1))
, t(b(x1)) -> b(s(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(b(x1)) -> b(s(s(s(x1))))
, t^#(s(x1)) -> c_5(t^#(t(x1)))}
Weak Rules:
{ s(b(s(x1))) -> b(t(x1))
, t^#(b(s(x1))) -> c_3(t^#(b(x1)))
, b(u(x1)) -> b(s(x1))
, s(u(x1)) -> s(s(x1))
, t^#(u(x1)) -> c_6(t^#(x1))
, t(b(x1)) -> b(s(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ u_0(4) -> 4
, t^#_0(4) -> 9
, c_6_0(9) -> 9}
5) { s^#(u(x1)) -> c_7(s^#(s(x1)))
, s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
The usable rules for this path are the following:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [4]
s^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [8]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
and weakly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [8]
s^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [4]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [4]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [7]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(u(x1)) -> u(t(x1))}
Weak Rules:
{ s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(u(x1)) -> u(t(x1))}
Weak Rules:
{ s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, b^#(u(x1)) -> c_4(b^#(s(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ s_0(4) -> 9
, s_0(9) -> 9
, u_0(4) -> 4
, s^#_0(4) -> 5
, s^#_0(9) -> 8
, b^#_0(4) -> 7
, b^#_0(9) -> 10
, c_4_0(10) -> 7
, c_7_0(8) -> 5}
6) { s^#(u(x1)) -> c_7(s^#(s(x1)))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
The usable rules for this path are the following:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [1]
s^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [1]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{t(b(s(x1))) -> u(t(b(x1)))}
and weakly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{t(b(s(x1))) -> u(t(b(x1)))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [1] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
Weak Rules:
{ t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, t(b(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s(u(x1)) -> s(s(x1))
, b(u(x1)) -> b(s(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
Weak Rules:
{ t(b(s(x1))) -> u(t(b(x1)))
, s(b(s(x1))) -> b(t(x1))
, t(s(x1)) -> t(t(x1))
, s^#(b(s(x1))) -> c_1(b^#(t(x1)))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ s_1(4) -> 9
, s_1(9) -> 9
, u_0(4) -> 4
, s^#_0(4) -> 5
, s^#_1(9) -> 8
, b^#_0(4) -> 7
, c_7_1(8) -> 5}
7) { s^#(u(x1)) -> c_7(s^#(s(x1)))
, s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
The usable rules for this path are the following:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))
, s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [0]
c_0(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [2]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
and weakly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [1]
u(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [0]
b^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
Weak Rules:
{ s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))
, s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
Weak Rules:
{ s^#(b(x1)) -> c_0(b^#(s(s(s(x1)))))
, s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ s_1(4) -> 9
, s_1(9) -> 9
, u_0(4) -> 4
, s^#_0(4) -> 5
, s^#_1(9) -> 8
, b^#_0(4) -> 7
, c_7_1(8) -> 5}
8) {s^#(u(x1)) -> c_7(s^#(s(x1)))}
The usable rules for this path are the following:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(b(s(x1))) -> b(t(x1))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, b(u(x1)) -> b(s(x1))
, t(s(x1)) -> t(t(x1))
, t(u(x1)) -> u(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
Details:
Interpretation Functions:
s(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
t(x1) = [1] x1 + [0]
u(x1) = [1] x1 + [0]
s^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
t^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
Weak Rules:
{ s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ s(b(x1)) -> b(s(s(s(x1))))
, s(u(x1)) -> s(s(x1))
, t(b(x1)) -> b(s(x1))
, b(u(x1)) -> b(s(x1))
, t(u(x1)) -> u(t(x1))
, s^#(u(x1)) -> c_7(s^#(s(x1)))}
Weak Rules:
{ s(b(s(x1))) -> b(t(x1))
, t(b(s(x1))) -> u(t(b(x1)))
, t(s(x1)) -> t(t(x1))}
Details:
The problem is Match-bounded by 1.
The enriched problem is compatible with the following automaton:
{ s_1(4) -> 7
, s_1(7) -> 7
, u_0(4) -> 4
, s^#_0(4) -> 5
, s^#_1(7) -> 6
, c_7_1(6) -> 5}